\begin{tabbing}
(\=Auto$\cdot$) \+
\\[0ex]CollapseTHEN ((RWO "p{-}fun{-}exp{-}compose" 0) 
\\[0ex]CollapseTHEN ((Auto') 
\\[0ex]
\\[0ex]CollapseTHEN ((Unfold `p{-}fun{-}exp` ( 0)$\cdot$) 
\\[0ex]CollapseTHEN ((GenConcl p{-}id() = ${\it id}$ THENA Auto
\-\\[0ex])\= \+
\\[0ex]CollapseTHEN (RWO "primrec\_add" 0 THEN Auto THEN Reduce 0 THEN Auto)$\cdot$)$\cdot$)$\cdot$)$\cdot$)$\cdot$
\-
\end{tabbing}